Step of Proof: p-mu-exists
11,40
postcript
pdf
Inference at
*
2
I
of proof for Lemma
p-mu-exists
:
1.
P
:
2.
(
n
:
. (
(
P
(
n
))))
x
:
+ Top. p-mu(
P
;
x
)
latex
by (InstConcl [inr
])
CollapseTHEN ((Auto
)
CollapseTHEN ((UnfoldTopAb 0)
CollapseTHEN ((
C
Reduce 0)
CollapseTHEN ((Auto
)
CollapseTHEN ((ParallelOp ( -2)
)
CollapseTHEN ((InstConcl [
C
i
])
CollapseTHEN (Auto
)
)
)
)
)
)
)
latex
C
.
Definitions
inr
x
,
,
p-mu(
P
;
x
)
,
,
{
x
:
A
|
B
(
x
)}
,
,
A
B
,
Void
,
x
:
A
B
(
x
)
,
A
,
P
Q
,
False
,
x
:
A
.
B
(
x
)
,
b
,
x
:
A
.
B
(
x
)
,
f
(
a
)
,
t
T
Lemmas
assert
wf
origin